Inference at * 2 1 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. ||l1||  ||l2||
5. i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)])
  L:T List. (l2 = (L @ l1)) 

latex

 by ((InstConcl [firstn(||l2|| - ||l1||;l2)]) 
CollapseTHENA (Auto')) 

latex

C1: 

C1:   l2 = (firstn(||l2|| - ||l1||;l2) @ l1)
C.

Definitions	firstn(n;as), n - m, ||as||, x:A. B(x), x:A  B(x), A  B, Type, type List, , as @ bs, x:A. B(x), x:AB(x), s = t, t  T
Lemmas	firstn wf, append wf